$\forall$${\it es}$:event\_system\{i:l\}, $L$:(Id List), $e$:es{-}E(${\it es}$).
\\[0ex]f{-}msg\{wanted:ut2, free:ut2, z:ut2\}(${\it es}$; $L$; $e$) $\in$ prop\{i:l\}